Report for no_context/combo2.c

Generated on 2023-06-28 04:21:14 by CPAchecker 2.2 / svcomp23

Matches in value-assignements (V): {{numOfValueMatches}}

Matches in edge-description: {{numOfDescriptionMatches}}

Rank
Scope
-V-
{{line.bestrank}}
{{line.desc}}
Precondition (initial variable assignment):

{{precondition}}

{{fault.rank}}. {{fault.score}} Details:
Current values:
Name Value
1
// Automatically generated by cegarmc  
2
//  
3
  
4
  
5
extern void __VERIFIER_assume(int);  
6
extern int __VERIFIER_nondet_bool();  
7
extern char __VERIFIER_nondet_char();  
8
extern signed char __VERIFIER_nondet_schar();  
9
extern unsigned char __VERIFIER_nondet_uchar();  
10
extern int __VERIFIER_nondet_int();  
11
extern unsigned int __VERIFIER_nondet_uint();  
12
extern short __VERIFIER_nondet_short();  
13
extern unsigned short __VERIFIER_nondet_ushort();  
14
extern long __VERIFIER_nondet_long();  
15
extern unsigned long __VERIFIER_nondet_ulong();  
16
extern long long __VERIFIER_nondet_longlong();  
17
extern unsigned long long __VERIFIER_nondet_ull();  
18
extern float __VERIFIER_nondet_float();  
19
extern double __VERIFIER_nondet_double();  
20
extern long double __VERIFIER_nondet_longdouble();  
21
extern void * __VERIFIER_nondet_pointer();  
22
  
23
int D_print_i;  
24
int D_print_st;  
25
int D_z;  
26
int N_generate_i;  
27
int N_generate_st;  
28
int S1_addsub_i;  
29
int S1_addsub_st;  
30
int S2_presdbl_i;  
31
int S2_presdbl_st;  
32
int S3_zero_i;  
33
int S3_zero_st;  
34
int count;  
35
int main_clk_ev;  
36
int main_clk_neg_edge;  
37
int main_clk_pos_edge;  
38
int main_clk_req_up;  
39
int main_clk_val;  
40
int main_clk_val_t;  
41
int main_dbl_ev;  
42
int main_dbl_req_up;  
43
int main_dbl_val;  
44
int main_dbl_val_t;  
45
int main_diff_ev;  
46
int main_diff_req_up;  
47
int main_diff_val;  
48
int main_diff_val_t;  
49
int main_in1_ev;  
50
int main_in1_req_up;  
51
int main_in1_val;  
52
int main_in1_val_t;  
53
int main_in2_ev;  
54
int main_in2_req_up;  
55
int main_in2_val;  
56
int main_in2_val_t;  
57
int main_pres_ev;  
58
int main_pres_req_up;  
59
int main_pres_val;  
60
int main_pres_val_t;  
61
int main_sum_ev;  
62
int main_sum_req_up;  
63
int main_sum_val;  
64
int main_sum_val_t;  
65
int main_zero_ev;  
66
int main_zero_req_up;  
67
int main_zero_val;  
68
int main_zero_val_t;  
69
int modFlag;  
70
int res;  
71
  
72
void error();  
73
void N_generate();  
74
void S1_addsub();  
75
void S2_presdbl();  
76
void S3_zero();  
77
void D_print();  
78
void eval();  
79
void start_simulation();  
80
  
81
  
82
void error() {  
83
  {  
84
  goto ERROR;  
85
  ERROR: ;  
86
  return;  
87
  }  
88
}  
89
  
90
void N_generate() {  
91
  auto int a;  
92
  auto int b;  
93
  {  
94
    main_in1_val_t = __VERIFIER_nondet_int();  
95
  main_in1_req_up = 1;  
96
    main_in2_val_t = __VERIFIER_nondet_int();  
97
  main_in2_req_up = 1;  
98
  return;  
99
  }  
100
}  
101
  
102
void S1_addsub() {  
103
  auto int a;  
104
  auto int b;  
105
  {  
106
  a = main_in1_val;  
107
  b = main_in2_val;  
108
  main_sum_val_t = a + b;  
109
  main_sum_req_up = 1;  
110
  main_diff_val_t = a - b;  
111
  main_diff_req_up = 1;  
112
  return;  
113
  }  
114
}  
115
  
116
void S2_presdbl() {  
117
  auto int a;  
118
  auto int b;  
119
  auto int c;  
120
  auto int d;  
121
  {  
122
  a = main_sum_val;  
123
  b = main_diff_val;  
124
  main_pres_val_t = a;  
125
  main_pres_req_up = 1;  
126
  c = a + b;  
127
  d = a - b;  
128
  main_dbl_val_t = c + d;  
129
  main_dbl_req_up = 1;  
130
  return;  
131
  }  
132
}  
133
  
134
void S3_zero() {  
135
  auto int a;  
136
  auto int b;  
137
  {  
138
  a = main_pres_val;  
139
  b = main_dbl_val;  
140
  main_zero_val_t = b - (a + a);  
141
  main_zero_req_up = 1;  
142
  return;  
143
  }  
144
}  
145
  
146
void D_print() {  
147
  {  
148
  D_z = main_zero_val;  
149
  return;  
150
  }  
151
}  
152
  
153
void eval() {  
154
  auto int tmp;  
155
  auto int tmp___0;  
156
  auto int tmp___1;  
157
  auto int tmp___2;  
158
  auto int tmp___3;  
159
  {  
160
  {  
161
    while (1) {  
162
      {  
163
        while_0_continue: ;  
164
        if (N_generate_st == 0) {  
165
          }  
166
        else {  
167
          if (S1_addsub_st == 0) {  
168
            }  
169
          else {  
170
            if (S2_presdbl_st == 0) {  
171
              }  
172
            else {  
173
              if (S3_zero_st == 0) {  
174
                }  
175
              else {  
176
                if (D_print_st == 0) {  
177
                  }  
178
                else {  
179
                  goto while_0_break;  
180
                  }  
181
                }  
182
              }  
183
            }  
184
          }  
185
        if (N_generate_st == 0) {  
186
          {  
187
                        tmp = __VERIFIER_nondet_int();  
188
            }  
189
          if (tmp) {  
190
            N_generate_st = 1;  
191
                        N_generate();  
192
            }  
193
          else {  
194
            }  
195
          }  
196
        else {  
197
          }  
198
        if (S1_addsub_st == 0) {  
199
          {  
200
                        tmp___0 = __VERIFIER_nondet_int();  
201
            }  
202
          if (tmp___0) {  
203
            S1_addsub_st = 1;  
204
                        S1_addsub();  
205
            }  
206
          else {  
207
            }  
208
          }  
209
        else {  
210
          }  
211
        if (S2_presdbl_st == 0) {  
212
          {  
213
                        tmp___1 = __VERIFIER_nondet_int();  
214
            }  
215
          if (tmp___1) {  
216
            S2_presdbl_st = 1;  
217
                        S2_presdbl();  
218
            }  
219
          else {  
220
            }  
221
          }  
222
        else {  
223
          }  
224
        if (S3_zero_st == 0) {  
225
          {  
226
                        tmp___2 = __VERIFIER_nondet_int();  
227
            }  
228
          if (tmp___2) {  
229
            S3_zero_st = 1;  
230
                        S3_zero();  
231
            }  
232
          else {  
233
            }  
234
          }  
235
        else {  
236
          }  
237
        if (D_print_st == 0) {  
238
          {  
239
                        tmp___3 = __VERIFIER_nondet_int();  
240
            }  
241
          if (tmp___3) {  
242
            D_print_st = 1;  
243
                        D_print();  
244
            }  
245
          else {  
246
            }  
247
          }  
248
        else {  
249
          }  
250
        }  
251
      }  
252
    while_0_break: ;  
253
    }  
254
  return;  
255
  }  
256
}  
257
  
258
void start_simulation() {  
259
  auto int kernel_st;  
260
  {  
261
  kernel_st = 0;  
262
  if (main_in1_req_up == 1) {  
263
    if (main_in1_val != main_in1_val_t) {  
264
      main_in1_val = main_in1_val_t;  
265
      main_in1_ev = 0;  
266
      }  
267
    else {  
268
      }  
269
    main_in1_req_up = 0;  
270
    }  
271
  else {  
272
    }  
273
  if (main_in2_req_up == 1) {  
274
    if (main_in2_val != main_in2_val_t) {  
275
      main_in2_val = main_in2_val_t;  
276
      main_in2_ev = 0;  
277
      }  
278
    else {  
279
      }  
280
    main_in2_req_up = 0;  
281
    }  
282
  else {  
283
    }  
284
  if (main_sum_req_up == 1) {  
285
    if (main_sum_val != main_sum_val_t) {  
286
      main_sum_val = main_sum_val_t;  
287
      main_sum_ev = 0;  
288
      }  
289
    else {  
290
      }  
291
    main_sum_req_up = 0;  
292
    }  
293
  else {  
294
    }  
295
  if (main_diff_req_up == 1) {  
296
    if (main_diff_val != main_diff_val_t) {  
297
      main_diff_val = main_diff_val_t;  
298
      main_diff_ev = 0;  
299
      }  
300
    else {  
301
      }  
302
    main_diff_req_up = 0;  
303
    }  
304
  else {  
305
    }  
306
  if (main_pres_req_up == 1) {  
307
    if (main_pres_val != main_pres_val_t) {  
308
      main_pres_val = main_pres_val_t;  
309
      main_pres_ev = 0;  
310
      }  
311
    else {  
312
      }  
313
    main_pres_req_up = 0;  
314
    }  
315
  else {  
316
    }  
317
  if (main_dbl_req_up == 1) {  
318
    if (main_dbl_val != main_dbl_val_t) {  
319
      main_dbl_val = main_dbl_val_t;  
320
      main_dbl_ev = 0;  
321
      }  
322
    else {  
323
      }  
324
    main_dbl_req_up = 0;  
325
    }  
326
  else {  
327
    }  
328
  if (main_zero_req_up == 1) {  
329
    if (main_zero_val != main_zero_val_t) {  
330
      main_zero_val = main_zero_val_t;  
331
      main_zero_ev = 0;  
332
      }  
333
    else {  
334
      }  
335
    main_zero_req_up = 0;  
336
    }  
337
  else {  
338
    }  
339
  if (main_clk_req_up == 1) {  
340
    if (main_clk_val != main_clk_val_t) {  
341
      main_clk_val = main_clk_val_t;  
342
      main_clk_ev = 0;  
343
      if (main_clk_val == 1) {  
344
        main_clk_pos_edge = 0;  
345
        main_clk_neg_edge = 2;  
346
        }  
347
      else {  
348
        main_clk_neg_edge = 0;  
349
        main_clk_pos_edge = 2;  
350
        }  
351
      }  
352
    else {  
353
      }  
354
    main_clk_req_up = 0;  
355
    }  
356
  else {  
357
    }  
358
  if (N_generate_i == 1) {  
359
    N_generate_st = 0;  
360
    }  
361
  else {  
362
    N_generate_st = 2;  
363
    }  
364
  if (S1_addsub_i == 1) {  
365
    S1_addsub_st = 0;  
366
    }  
367
  else {  
368
    S1_addsub_st = 2;  
369
    }  
370
  if (S2_presdbl_i == 1) {  
371
    S2_presdbl_st = 0;  
372
    }  
373
  else {  
374
    S2_presdbl_st = 2;  
375
    }  
376
  if (S3_zero_i == 1) {  
377
    S3_zero_st = 0;  
378
    }  
379
  else {  
380
    S3_zero_st = 2;  
381
    }  
382
  if (D_print_i == 1) {  
383
    D_print_st = 0;  
384
    }  
385
  else {  
386
    D_print_st = 2;  
387
    }  
388
  if (main_in1_ev == 0) {  
389
    main_in1_ev = 1;  
390
    }  
391
  else {  
392
    }  
393
  if (main_in2_ev == 0) {  
394
    main_in2_ev = 1;  
395
    }  
396
  else {  
397
    }  
398
  if (main_sum_ev == 0) {  
399
    main_sum_ev = 1;  
400
    }  
401
  else {  
402
    }  
403
  if (main_diff_ev == 0) {  
404
    main_diff_ev = 1;  
405
    }  
406
  else {  
407
    }  
408
  if (main_pres_ev == 0) {  
409
    main_pres_ev = 1;  
410
    }  
411
  else {  
412
    }  
413
  if (main_dbl_ev == 0) {  
414
    main_dbl_ev = 1;  
415
    }  
416
  else {  
417
    }  
418
  if (main_zero_ev == 0) {  
419
    main_zero_ev = 1;  
420
    }  
421
  else {  
422
    }  
423
  if (main_clk_ev == 0) {  
424
    main_clk_ev = 1;  
425
    }  
426
  else {  
427
    }  
428
  if (main_clk_pos_edge == 0) {  
429
    main_clk_pos_edge = 1;  
430
    }  
431
  else {  
432
    }  
433
  if (main_clk_neg_edge == 0) {  
434
    main_clk_neg_edge = 1;  
435
    }  
436
  else {  
437
    }  
438
  if (main_clk_pos_edge == 1) {  
439
    N_generate_st = 0;  
440
    }  
441
  else {  
442
    }  
443
  if (main_clk_pos_edge == 1) {  
444
    S1_addsub_st = 0;  
445
    }  
446
  else {  
447
    }  
448
  if (main_clk_pos_edge == 1) {  
449
    S2_presdbl_st = 0;  
450
    }  
451
  else {  
452
    }  
453
  if (main_clk_pos_edge == 1) {  
454
    S3_zero_st = 0;  
455
    }  
456
  else {  
457
    }  
458
  if (main_clk_pos_edge == 1) {  
459
    D_print_st = 0;  
460
    }  
461
  else {  
462
    }  
463
  if (main_in1_ev == 1) {  
464
    main_in1_ev = 2;  
465
    }  
466
  else {  
467
    }  
468
  if (main_in2_ev == 1) {  
469
    main_in2_ev = 2;  
470
    }  
471
  else {  
472
    }  
473
  if (main_sum_ev == 1) {  
474
    main_sum_ev = 2;  
475
    }  
476
  else {  
477
    }  
478
  if (main_diff_ev == 1) {  
479
    main_diff_ev = 2;  
480
    }  
481
  else {  
482
    }  
483
  if (main_pres_ev == 1) {  
484
    main_pres_ev = 2;  
485
    }  
486
  else {  
487
    }  
488
  if (main_dbl_ev == 1) {  
489
    main_dbl_ev = 2;  
490
    }  
491
  else {  
492
    }  
493
  if (main_zero_ev == 1) {  
494
    main_zero_ev = 2;  
495
    }  
496
  else {  
497
    }  
498
  if (main_clk_ev == 1) {  
499
    main_clk_ev = 2;  
500
    }  
501
  else {  
502
    }  
503
  if (main_clk_pos_edge == 1) {  
504
    main_clk_pos_edge = 2;  
505
    }  
506
  else {  
507
    }  
508
  if (main_clk_neg_edge == 1) {  
509
    main_clk_neg_edge = 2;  
510
    }  
511
  else {  
512
    }  
513
  {  
514
    while (1) {  
515
      {  
516
        while_1_continue: ;  
517
        {  
518
          kernel_st = 1;  
519
                    eval();  
520
          }  
521
        kernel_st = 2;  
522
        if (main_in1_req_up == 1) {  
523
          if (main_in1_val != main_in1_val_t) {  
524
            main_in1_val = main_in1_val_t;  
525
            main_in1_ev = 0;  
526
            }  
527
          else {  
528
            }  
529
          main_in1_req_up = 0;  
530
          }  
531
        else {  
532
          }  
533
        if (main_in2_req_up == 1) {  
534
          if (main_in2_val != main_in2_val_t) {  
535
            main_in2_val = main_in2_val_t;  
536
            main_in2_ev = 0;  
537
            }  
538
          else {  
539
            }  
540
          main_in2_req_up = 0;  
541
          }  
542
        else {  
543
          }  
544
        if (main_sum_req_up == 1) {  
545
          if (main_sum_val != main_sum_val_t) {  
546
            main_sum_val = main_sum_val_t;  
547
            main_sum_ev = 0;  
548
            }  
549
          else {  
550
            }  
551
          main_sum_req_up = 0;  
552
          }  
553
        else {  
554
          }  
555
        if (main_diff_req_up == 1) {  
556
          if (main_diff_val != main_diff_val_t) {  
557
            main_diff_val = main_diff_val_t;  
558
            main_diff_ev = 0;  
559
            }  
560
          else {  
561
            }  
562
          main_diff_req_up = 0;  
563
          }  
564
        else {  
565
          }  
566
        if (main_pres_req_up == 1) {  
567
          if (main_pres_val != main_pres_val_t) {  
568
            main_pres_val = main_pres_val_t;  
569
            main_pres_ev = 0;  
570
            }  
571
          else {  
572
            }  
573
          main_pres_req_up = 0;  
574
          }  
575
        else {  
576
          }  
577
        if (main_dbl_req_up == 1) {  
578
          if (main_dbl_val != main_dbl_val_t) {  
579
            main_dbl_val = main_dbl_val_t;  
580
            main_dbl_ev = 0;  
581
            }  
582
          else {  
583
            }  
584
          main_dbl_req_up = 0;  
585
          }  
586
        else {  
587
          }  
588
        if (main_zero_req_up == 1) {  
589
          if (main_zero_val != main_zero_val_t) {  
590
            main_zero_val = main_zero_val_t;  
591
            main_zero_ev = 0;  
592
            }  
593
          else {  
594
            }  
595
          main_zero_req_up = 0;  
596
          }  
597
        else {  
598
          }  
599
        if (main_clk_req_up == 1) {  
600
          if (main_clk_val != main_clk_val_t) {  
601
            main_clk_val = main_clk_val_t;  
602
            main_clk_ev = 0;  
603
            if (main_clk_val == 1) {  
604
              main_clk_pos_edge = 0;  
605
              main_clk_neg_edge = 2;  
606
              }  
607
            else {  
608
              main_clk_neg_edge = 0;  
609
              main_clk_pos_edge = 2;  
610
              }  
611
            }  
612
          else {  
613
            }  
614
          main_clk_req_up = 0;  
615
          }  
616
        else {  
617
          }  
618
        kernel_st = 3;  
619
        if (main_in1_ev == 0) {  
620
          main_in1_ev = 1;  
621
          }  
622
        else {  
623
          }  
624
        if (main_in2_ev == 0) {  
625
          main_in2_ev = 1;  
626
          }  
627
        else {  
628
          }  
629
        if (main_sum_ev == 0) {  
630
          main_sum_ev = 1;  
631
          }  
632
        else {  
633
          }  
634
        if (main_diff_ev == 0) {  
635
          main_diff_ev = 1;  
636
          }  
637
        else {  
638
          }  
639
        if (main_pres_ev == 0) {  
640
          main_pres_ev = 1;  
641
          }  
642
        else {  
643
          }  
644
        if (main_dbl_ev == 0) {  
645
          main_dbl_ev = 1;  
646
          }  
647
        else {  
648
          }  
649
        if (main_zero_ev == 0) {  
650
          main_zero_ev = 1;  
651
          }  
652
        else {  
653
          }  
654
        if (main_clk_ev == 0) {  
655
          main_clk_ev = 1;  
656
          }  
657
        else {  
658
          }  
659
        if (main_clk_pos_edge == 0) {  
660
          main_clk_pos_edge = 1;  
661
          }  
662
        else {  
663
          }  
664
        if (main_clk_neg_edge == 0) {  
665
          main_clk_neg_edge = 1;  
666
          }  
667
        else {  
668
          }  
669
        if (main_clk_pos_edge == 1) {  
670
          N_generate_st = 0;  
671
          }  
672
        else {  
673
          }  
674
        if (main_clk_pos_edge == 1) {  
675
          S1_addsub_st = 0;  
676
          }  
677
        else {  
678
          }  
679
        if (main_clk_pos_edge == 1) {  
680
          S2_presdbl_st = 0;  
681
          }  
682
        else {  
683
          }  
684
        if (main_clk_pos_edge == 1) {  
685
          S3_zero_st = 0;  
686
          }  
687
        else {  
688
          }  
689
        if (main_clk_pos_edge == 1) {  
690
          D_print_st = 0;  
691
          }  
692
        else {  
693
          }  
694
        if (main_in1_ev == 1) {  
695
          main_in1_ev = 2;  
696
          }  
697
        else {  
698
          }  
699
        if (main_in2_ev == 1) {  
700
          main_in2_ev = 2;  
701
          }  
702
        else {  
703
          }  
704
        if (main_sum_ev == 1) {  
705
          main_sum_ev = 2;  
706
          }  
707
        else {  
708
          }  
709
        if (main_diff_ev == 1) {  
710
          main_diff_ev = 2;  
711
          }  
712
        else {  
713
          }  
714
        if (main_pres_ev == 1) {  
715
          main_pres_ev = 2;  
716
          }  
717
        else {  
718
          }  
719
        if (main_dbl_ev == 1) {  
720
          main_dbl_ev = 2;  
721
          }  
722
        else {  
723
          }  
724
        if (main_zero_ev == 1) {  
725
          main_zero_ev = 2;  
726
          }  
727
        else {  
728
          }  
729
        if (main_clk_ev == 1) {  
730
          main_clk_ev = 2;  
731
          }  
732
        else {  
733
          }  
734
        if (main_clk_pos_edge == 1) {  
735
          main_clk_pos_edge = 2;  
736
          }  
737
        else {  
738
          }  
739
        if (main_clk_neg_edge == 1) {  
740
          main_clk_neg_edge = 2;  
741
          }  
742
        else {  
743
          }  
744
        if (N_generate_st == 0) {  
745
          }  
746
        else {  
747
          if (S1_addsub_st == 0) {  
748
            }  
749
          else {  
750
            if (S2_presdbl_st == 0) {  
751
              }  
752
            else {  
753
              if (S3_zero_st == 0) {  
754
                }  
755
              else {  
756
                if (D_print_st == 0) {  
757
                  }  
758
                else {  
759
                  goto while_1_break;  
760
                  }  
761
                }  
762
              }  
763
            }  
764
          }  
765
        }  
766
      }  
767
    while_1_break: ;  
768
    }  
769
  return;  
770
  }  
771
}  
772
  
773
void main () {  
774
//  
775
// Number of lvals: 62  
776
//   Frama_C_interval: int (int min, int max)  
777
//      int (int min, int max)  
778
//   error: void (void)  
779
//      void (void)  
780
//   count: int  
781
//      int  
782
//   res: int  
783
//      int  
784
//   modFlag: int  
785
//      int  
786
//   main_in1_val: int  
787
//      int  
788
//   main_in1_val_t: int  
789
//      int  
790
//   main_in1_ev: int  
791
//      int  
792
//   main_in1_req_up: int  
793
//      int  
794
//   main_in2_val: int  
795
//      int  
796
//   main_in2_val_t: int  
797
//      int  
798
//   main_in2_ev: int  
799
//      int  
800
//   main_in2_req_up: int  
801
//      int  
802
//   main_diff_val: int  
803
//      int  
804
//   main_diff_val_t: int  
805
//      int  
806
//   main_diff_ev: int  
807
//      int  
808
//   main_diff_req_up: int  
809
//      int  
810
//   main_sum_val: int  
811
//      int  
812
//   main_sum_val_t: int  
813
//      int  
814
//   main_sum_ev: int  
815
//      int  
816
//   main_sum_req_up: int  
817
//      int  
818
//   main_pres_val: int  
819
//      int  
820
//   main_pres_val_t: int  
821
//      int  
822
//   main_pres_ev: int  
823
//      int  
824
//   main_pres_req_up: int  
825
//      int  
826
//   main_dbl_val: int  
827
//      int  
828
//   main_dbl_val_t: int  
829
//      int  
830
//   main_dbl_ev: int  
831
//      int  
832
//   main_dbl_req_up: int  
833
//      int  
834
//   main_zero_val: int  
835
//      int  
836
//   main_zero_val_t: int  
837
//      int  
838
//   main_zero_ev: int  
839
//      int  
840
//   main_zero_req_up: int  
841
//      int  
842
//   main_clk_val: int  
843
//      int  
844
//   main_clk_val_t: int  
845
//      int  
846
//   main_clk_ev: int  
847
//      int  
848
//   main_clk_req_up: int  
849
//      int  
850
//   main_clk_pos_edge: int  
851
//      int  
852
//   main_clk_neg_edge: int  
853
//      int  
854
//   N_generate_st: int  
855
//      int  
856
//   N_generate_i: int  
857
//      int  
858
//   S1_addsub_st: int  
859
//      int  
860
//   S1_addsub_i: int  
861
//      int  
862
//   S2_presdbl_st: int  
863
//      int  
864
//   S2_presdbl_i: int  
865
//      int  
866
//   S3_zero_st: int  
867
//      int  
868
//   S3_zero_i: int  
869
//      int  
870
//   D_z: int  
871
//      int  
872
//   D_print_st: int  
873
//      int  
874
//   D_print_i: int  
875
//      int  
876
//   N_generate: void (void)  
877
//      void (void)  
878
//   S1_addsub: void (void)  
879
//      void (void)  
880
//   S2_presdbl: void (void)  
881
//      void (void)  
882
//   S3_zero: void (void)  
883
//      void (void)  
884
//   D_print: void (void)  
885
//      void (void)  
886
//   eval: void (void)  
887
//      void (void)  
888
//   start_simulation: void (void)  
889
//      void (void)  
890
//   n1: int  
891
//      int  
892
//   n2: int  
893
//      int  
894
//   n3: int  
895
//      int  
896
//   bound: int  
897
//      int  
898
//   i: int  
899
//      int  
900
//  
901
  
902
D_print_i = __VERIFIER_nondet_int();  
903
D_print_st = __VERIFIER_nondet_int();  
904
D_z = __VERIFIER_nondet_int();  
905
N_generate_i = __VERIFIER_nondet_int();  
906
N_generate_st = __VERIFIER_nondet_int();  
907
S1_addsub_i = __VERIFIER_nondet_int();  
908
S1_addsub_st = __VERIFIER_nondet_int();  
909
S2_presdbl_i = __VERIFIER_nondet_int();  
910
S2_presdbl_st = __VERIFIER_nondet_int();  
911
S3_zero_i = __VERIFIER_nondet_int();  
912
S3_zero_st = __VERIFIER_nondet_int();  
913
count = __VERIFIER_nondet_int();  
914
main_clk_ev = __VERIFIER_nondet_int();  
915
main_clk_neg_edge = __VERIFIER_nondet_int();  
916
main_clk_pos_edge = __VERIFIER_nondet_int();  
917
main_clk_req_up = __VERIFIER_nondet_int();  
918
main_clk_val = __VERIFIER_nondet_int();  
919
main_clk_val_t = __VERIFIER_nondet_int();  
920
main_dbl_ev = __VERIFIER_nondet_int();  
921
main_dbl_req_up = __VERIFIER_nondet_int();  
922
main_dbl_val = __VERIFIER_nondet_int();  
923
main_dbl_val_t = __VERIFIER_nondet_int();  
924
main_diff_ev = __VERIFIER_nondet_int();  
925
main_diff_req_up = __VERIFIER_nondet_int();  
926
main_diff_val = __VERIFIER_nondet_int();  
927
main_diff_val_t = __VERIFIER_nondet_int();  
928
main_in1_ev = __VERIFIER_nondet_int();  
929
main_in1_req_up = __VERIFIER_nondet_int();  
930
main_in1_val = __VERIFIER_nondet_int();  
931
main_in1_val_t = __VERIFIER_nondet_int();  
932
main_in2_ev = __VERIFIER_nondet_int();  
933
main_in2_req_up = __VERIFIER_nondet_int();  
934
main_in2_val = __VERIFIER_nondet_int();  
935
main_in2_val_t = __VERIFIER_nondet_int();  
936
main_pres_ev = __VERIFIER_nondet_int();  
937
main_pres_req_up = __VERIFIER_nondet_int();  
938
main_pres_val = __VERIFIER_nondet_int();  
939
main_pres_val_t = __VERIFIER_nondet_int();  
940
main_sum_ev = __VERIFIER_nondet_int();  
941
main_sum_req_up = __VERIFIER_nondet_int();  
942
main_sum_val = __VERIFIER_nondet_int();  
943
main_sum_val_t = __VERIFIER_nondet_int();  
944
main_zero_ev = __VERIFIER_nondet_int();  
945
main_zero_req_up = __VERIFIER_nondet_int();  
946
main_zero_val = __VERIFIER_nondet_int();  
947
main_zero_val_t = __VERIFIER_nondet_int();  
948
modFlag = __VERIFIER_nondet_int();  
949
res = __VERIFIER_nondet_int();  
950
  
951
  
952
  
953
{  
954
  int n1 = 3;  
955
  int n2 = 5;  
956
  int n3 = 7;  
957
  res = 0;  
958
  auto int bound;  
959
  bound = __VERIFIER_nondet_int();  
960
  {  
961
    int i = 0;  
962
    while (1) {  
963
      if (i < bound) {  
964
        }  
965
      else {  
966
        break;  
967
        }  
968
      {  
969
        if (i % n1 == 0) {  
970
          if (i % n2 == 0) {  
971
            if (i % n3 == 0) {  
972
              res = i;  
973
              }  
974
            else {  
975
              }  
976
            }  
977
          else {  
978
            }  
979
          }  
980
        else {  
981
          }  
982
        }  
983
      i ++;  
984
      }  
985
    }  
986
  {  
987
    modFlag = res;  
988
    }  
989
  if (modFlag % 105 == 0) {  
990
    {  
991
      count = 0;  
992
      main_in1_ev = 2;  
993
      main_in1_req_up = 0;  
994
      main_in2_ev = 2;  
995
      main_in2_req_up = 0;  
996
      main_diff_ev = 2;  
997
      main_diff_req_up = 0;  
998
      main_sum_ev = 2;  
999
      main_sum_req_up = 0;  
1000
      main_pres_ev = 2;  
1001
      main_pres_req_up = 0;  
1002
      main_dbl_ev = 2;  
1003
      main_dbl_req_up = 0;  
1004
      main_zero_ev = 2;  
1005
      main_zero_req_up = 0;  
1006
      main_clk_val = 0;  
1007
      main_clk_ev = 2;  
1008
      main_clk_req_up = 0;  
1009
      main_clk_pos_edge = 2;  
1010
      main_clk_neg_edge = 2;  
1011
      count = 0;  
1012
      N_generate_i = 0;  
1013
      S1_addsub_i = 0;  
1014
      S2_presdbl_i = 0;  
1015
      S3_zero_i = 0;  
1016
      D_print_i = 0;  
1017
            start_simulation();  
1018
      }  
1019
    {  
1020
      while (1) {  
1021
        {  
1022
          while_2_continue: ;  
1023
          {  
1024
            main_clk_val_t = 1;  
1025
            main_clk_req_up = 1;  
1026
                        start_simulation();  
1027
            count ++;  
1028
            }  
1029
          if (count == 5) {  
1030
            if (! (D_z == 0)) {  
1031
                            error();  
1032
              }  
1033
            else {  
1034
              }  
1035
            count = 0;  
1036
            }  
1037
          else {  
1038
            }  
1039
          {  
1040
            main_clk_val_t = 0;  
1041
            main_clk_req_up = 1;  
1042
                        start_simulation();  
1043
            }  
1044
          }  
1045
        }  
1046
      }  
1047
    }  
1048
  else {  
1049
        error();  
1050
    }  
1051
  }  
1052
return;  
1053
}  
DateTimeLevelComponentMessage
2023-06-2804:19:09:396INFOCPAMain.detectFrontendLanguageIfNecessaryLanguage C detected and set for analysis
2023-06-2804:19:09:413INFOResourceLimitChecker.fromConfigurationUsing the following resource limits: CPU-time limit of 900s
2023-06-2804:19:09:467INFOCPAchecker.runCPAchecker 2.2 / svcomp23 (OpenJDK 64-Bit Server VM 11.0.19) started
2023-06-2804:19:09:484INFOCPAchecker.parseParsing CFA from file(s) "no_context/combo2.c"
2023-06-2804:19:10:457INFOCoreComponentsFactory.createAlgorithmUsing heuristics to select analysis
2023-06-2804:19:10:469WARNINGCPAchecker.printConfigurationWarningsThe following configuration options were specified but are not used:
cpa.callstack.unsupportedFunctions
termination.violation.witness
cpa.predicate.memoryAllocationsAlwaysSucceed
cpa.arg.compressWitness
cpa.callstack.skipFunctionPointerRecursion
cpa.composite.aggregateBasicBlocks
counterexample.export.graphml
counterexample.export.compressWitness
cpa.arg.proofWitness
2023-06-2804:19:10:469INFOCPAchecker.runAlgorithmStarting analysis ...
2023-06-2804:19:10:473INFOSelectionAlgorithm.chooseConfigPerforming heuristic ...
2023-06-2804:19:10:477INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
ResourceLimitChecker.fromConfiguration
Using the following resource limits: CPU-time limit of 900s
2023-06-2804:19:10:502INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
CoreComponentsFactory.createAlgorithm
Using Restarting Algorithm
2023-06-2804:19:10:508INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
RestartAlgorithm.run
Loading analysis 1 from file /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties ...
2023-06-2804:19:10:513INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
NestingAlgorithm.checkConfigs
Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties': 'cpa.composite.aggregateBasicBlocks' has two values 'false' and 'true'. Using 'true'.
2023-06-2804:19:10:513INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
NestingAlgorithm.checkConfigs
Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties': 'limits.time.cpu' has two values '900s' and '140s'. Using '140s'.
2023-06-2804:19:10:513INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
NestingAlgorithm.checkConfigs
Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties': 'limits.time.cpu::required' has two values '900' and '140s'. Using '140s'.
2023-06-2804:19:10:514INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties
ResourceLimitChecker.fromConfiguration
Using the following resource limits: CPU-time limit of 140s
2023-06-2804:19:10:809INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
RestartAlgorithm.run
Starting analysis 1 ...
2023-06-2804:21:12:614WARNINGAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
ShutdownNotifier.shutdownIfNecessary
Warning: Analysis 1 stopped. (The CPU-time limit of 140s has elapsed.)
2023-06-2804:21:12:956INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
RestartAlgorithm.run
RestartAlgorithm switches to the next configuration...
2023-06-2804:21:12:957INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
RestartAlgorithm.run
Loading analysis 2 from file /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties ...
2023-06-2804:21:12:960INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
NestingAlgorithm.checkConfigs
Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties': 'cpa.composite.aggregateBasicBlocks' has two values 'false' and 'true'. Using 'true'.
2023-06-2804:21:12:960INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
NestingAlgorithm.checkConfigs
Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties': 'limits.time.cpu' has two values '900s' and '60s'. Using '60s'.
2023-06-2804:21:12:961INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
NestingAlgorithm.checkConfigs
Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties': 'limits.time.cpu::required' has two values '900' and '60s'. Using '60s'.
2023-06-2804:21:12:961INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties
ResourceLimitChecker.fromConfiguration
Using the following resource limits: CPU-time limit of 60s
2023-06-2804:21:13:014INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
RestartAlgorithm.run
Starting analysis 2 ...
2023-06-2804:21:13:104INFOCPAchecker.runAlgorithmStopping analysis ...
Statistics NameStatistics ValueAdditional Value
Selection Algorithm statistics
Size of preliminary analysis reached set 0
Used algorithm property /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
Program containing only relevant bools 0
Relevant boolean vars / relevant vars ratio 0.0676
Requires alias handling 0
Requires loop handling 1
Has a single loop 0
Requires composite-type handling 0
Requires array handling 0
Requires float handling 0
Requires recursion handling 0
Relevant addressed vars / relevant vars ratio 0.0000
Program containing external functions true
Number of all righthand side functions 9
Restart Algorithm statistics
Number of algorithms provided 7
Number of algorithms used 2
Total time for algorithm 2 0.147s
ValueAnalysisCPA statistics
Number of variables per state 0.00 sum: 0, count: 1448, min: 0, max: 0
Number of global variables per state 0.00 sum: 0, count: 1448, min: 0, max: 0
Number of assumptions 668
Number of deterministic assumptions 0
Level of Determinism 0%
ValueAnalysisPrecisionAdjustment statistics
Number of abstraction computations 1781
Total time for liveness abstraction 0.000s
Total time for abstraction computation 0.007s
Total time for path thresholds 0.000s
ConstraintsStrengthenOperator statistics
Total time for strengthening by ConstraintsCPA 0.000s
Replaced symbolic expressions 0
AutomatonAnalysis (SVCOMP) statistics
Number of states 1
Total time for successor computation 0.001s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 2122, count: 2122, min: 1, max: 1 [1 x 2122]
Number of states with assumption transitions 0
CPA algorithm statistics
Number of iterations 1448
Max size of waitlist 27
Average size of waitlist 13
Number of computed successors 1781
Max successors for one state 2
Number of times merged 0
Number of times stopped 334
Number of times breaked 0
Total time for CPA algorithm 0.079s Max: 0.079s
Time for choose from waitlist 0.012s
Time for precision adjustment 0.014s
Time for transfer relation 0.029s
Time for stop operator 0.004s
Time for adding to reached set 0.010s
ValueAnalysisRefiner statistics
Number of refinements 0
Number of targets found 0 count: 0, min: 0, max: 0, avg: 0.00
Time for completing refinement 0.000s
Number of root relocations 0
Number of similar, repeated refinements 0
Number of unique precision increments 0
PathExtractor statistics
Total number of targets found 0
ValueAnalysisPathInterpolator statistics
Time for interpolation 0.000s
Number of interpolations 0
Number of interpolation queries 0 count: 0, min: 0, max: 0, avg: 0.00
Size of interpolant 0.00 sum: 0, count: 0, min: 0, max: 0
Number of sliced prefixes 0 count: 0, min: 0, max: 0, avg: 0.00
Extracting infeasible sliced prefixes 0.000s
Selecting infeasible sliced prefixes 0.000s
CEGAR algorithm statistics
Number of CEGAR refinements 0
Counterexample-Check Algorithm statistics
Number of counterexample checks 0
CPA algorithm statistics
Number of iterations 1448
Max size of waitlist 27
Average size of waitlist 13
Number of computed successors 1781
Max successors for one state 2
Number of times merged 0
Number of times stopped 334
Number of times breaked 0
Total time for CPA algorithm 0.079s Max: 0.079s
Time for choose from waitlist 0.012s
Time for precision adjustment 0.014s
Time for transfer relation 0.029s
Time for stop operator 0.004s
Time for adding to reached set 0.010s
ValueAnalysisRefiner statistics
Number of refinements 0
Number of targets found 0 count: 0, min: 0, max: 0, avg: 0.00
Time for completing refinement 0.000s
Number of root relocations 0
Number of similar, repeated refinements 0
Number of unique precision increments 0
PathExtractor statistics
Total number of targets found 0
ValueAnalysisPathInterpolator statistics
Time for interpolation 0.000s
Number of interpolations 0
Number of interpolation queries 0 count: 0, min: 0, max: 0, avg: 0.00
Size of interpolant 0.00 sum: 0, count: 0, min: 0, max: 0
Number of sliced prefixes 0 count: 0, min: 0, max: 0, avg: 0.00
Extracting infeasible sliced prefixes 0.000s
Selecting infeasible sliced prefixes 0.000s
CEGAR algorithm statistics
Number of CEGAR refinements 0
Counterexample-Check Algorithm statistics
Number of counterexample checks 0
Code Coverage
Function coverage 1.000
Visited lines 457
Total lines 457
Line coverage 1.000
Visited conditions 232
Total conditions 232
Condition coverage 1.000
CPAchecker general statistics
Number of program locations 734
Number of CFA edges (per node) 863 count: 734, min: 0, max: 3, avg: 1.18
Number of relevant variables 74
Number of functions 9
Number of loops (and loop nodes) 4 sum: 291, min: 17, max: 196, avg: 72.75
Size of reached set 1448
Number of reached locations 513 70%
Avg states per location 2
Max states per location 3 at node N7
Number of reached functions 9 100%
Number of target states 0
Time for analysis setup 0.985s
Time for loading CPAs 0.134s
Time for loading parser 0.146s
Time for CFA construction 0.678s
Time for parsing file(s) 0.258s
Time for AST to CFA 0.160s
Time for CFA sanity check 0.046s
Time for post-processing 0.150s
Time for CFA export 0.849s
Time for function pointers resolving 0.005s
Function calls via function pointers 0 count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer calls 0 count: 1, min: 0, max: 0, avg: 0.00
Function calls with function pointer arguments 0 count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer arguments 0 count: 1, min: 0, max: 0, avg: 0.00
Time for classifying variables 0.086s
Time for collecting variables 0.030s
Time for solving dependencies 0.001s
Time for building hierarchy 0.000s
Time for building classification 0.050s
Time for exporting data 0.005s
Time for Analysis 122.635s
CPU time for analysis 141.270s
Time for analyzing result 0.001s
Total time for CPAchecker 123.621s
Total CPU time for CPAchecker 144.150s
Time for statistics 0.054s
Time for Garbage Collector 1.302s in 57 runs
Garbage Collector(s) used G1 Old Generation, G1 Young Generation
Used heap memory 674MB ( 643 MiB) max; 323MB ( 308 MiB) avg; 693MB ( 660 MiB) peak
Used non-heap memory 54MB ( 51 MiB) max; 52MB ( 49 MiB) avg; 55MB ( 52 MiB) peak
Used in G1 Old Gen pool 163MB ( 155 MiB) max; 97MB ( 93 MiB) avg; 163MB ( 155 MiB) peak
Allocated heap memory 871MB ( 831 MiB) max; 721MB ( 688 MiB) avg
Allocated non-heap memory 57MB ( 54 MiB) max; 54MB ( 52 MiB) avg
Total process virtual memory 12222MB ( 11656 MiB) max; 12217MB ( 11651 MiB) avg
#Configuration NameConfiguration Value
1analysis.entryFunction main
2analysis.name svcomp23
3analysis.programNames no_context/combo2.c
4analysis.selectAnalysisHeuristically true
5analysis.summaryEdges true
6cfa.simplifyCfa false
7cfa.useCFACloningForMultiThreadedPrograms true
8counterexample.export.compressWitness false
9counterexample.export.graphml witness.graphml
10cpa.arg.compressWitness false
11cpa.arg.proofWitness witness.graphml
12cpa.callstack.skipFunctionPointerRecursion true
13cpa.callstack.unsupportedFunctions pthread_create,pthread_key_create,sin,cos,__builtin_uaddl_overflow
14cpa.composite.aggregateBasicBlocks false
15cpa.predicate.memoryAllocationsAlwaysSucceed true
16datarace.config svcomp23--datarace.properties
17heuristicSelection.addressedRatio 0.0
18heuristicSelection.complexLoopConfig components/svcomp23--configselection-restart-valueAnalysis-fallbacks.properties
19heuristicSelection.loopConfig components/svcomp23--multipleLoopsConfig.properties
20heuristicSelection.loopFreeConfig components/svcomp23--configselection-restart-bmc-fallbacks.properties
21heuristicSelection.singleLoopConfig components/svcomp23--singleLoopConfig.properties
22language C
23limits.time.cpu 900s
24limits.time.cpu::required 900
25log.level INFO
26memorycleanup.config svcomp23--memorycleanup.properties
27memorysafety.config svcomp23--memorysafety.properties
28overflow.config svcomp23--overflow.properties
29parser.usePreprocessor true
30specification /home/artjom/CPAchecker-2.2-unix/config/properties/unreach-call.prp
31statistics.print true
32termination.config svcomp23--termination.properties
33termination.violation.witness witness.graphml

About

This table was generated by CPAchecker. For feedback, questions, and bug reports please use our issue tracker.

License: Apache 2.0 License

This application includes third-party dependencies under different licenses. Click here to view them.

{{dependency.name}} {{dependency.version}}

Source: {{dependency.repository}}

{{dependency.copyright}}

License:

Full text of license
{{dependencies.licenses[dependency.licenseId]}}